\begin{tabbing}
$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$prop\{i:l\}).
\\[0ex]($\forall$$L$:($T$ List). decidable($P$($L$)))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:($T$ List). \+
\\[0ex]$P$($L$)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it L'}$:$T$ List\+
\\[0ex](iseg($T$; ${\it L'}$; $L$)
\\[0ex]$\wedge$ $P$(${\it L'}$)
\\[0ex]$\wedge$ ($\forall$${\it L''}$:($T$ List). iseg($T$; ${\it L''}$; ${\it L'}$) $\Rightarrow$ $P$(${\it L''}$) $\Rightarrow$ (${\it L''}$ = ${\it L'}$)))))
\-\-
\end{tabbing}